ma{-}single{-}pre{-}init1($x$;$T$;$c$;$a$;${\it T'}$;$y$,$v$.$P$($y$;$v$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$with ds: $x$ : $T$ init: $x$ : $c$action $a$:${\it T'}$ precondition $a$(v) is $\lambda$$s$,$v$. $P$($s$($x$);$v$)